Nuprl Lemma : flip_twice
4,23
postcript
pdf
k
:
,
x
,
y
,
i
:
k
. (
y
,
x
)((
y
,
x
)(
i
)) =
i
latex
Definitions
f
o
g
,
(
i
,
j
)
,
i
j
<
k
,
A
B
,
P
&
Q
,
A
,
False
,
P
Q
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
,
P
Q
Lemmas
flip
inverse
,
int
seg
wf
origin
k:
, x, y, i:
k. (y, x)((y, x)(i)) = i 
k:, x, y, i:k. (y, x)((y, x)(i)) = i 
j < kB
A
Q
}x:A. B(x) T
Q Q